qsort(nil) → nil
qsort(.(x, y)) → ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) → nil
lowers(x, .(y, z)) → if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) → nil
greaters(x, .(y, z)) → if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))
↳ QTRS
↳ DependencyPairsProof
qsort(nil) → nil
qsort(.(x, y)) → ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) → nil
lowers(x, .(y, z)) → if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) → nil
greaters(x, .(y, z)) → if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))
LOWERS(x, .(y, z)) → LOWERS(x, z)
GREATERS(x, .(y, z)) → GREATERS(x, z)
QSORT(.(x, y)) → GREATERS(x, y)
QSORT(.(x, y)) → LOWERS(x, y)
QSORT(.(x, y)) → QSORT(greaters(x, y))
QSORT(.(x, y)) → QSORT(lowers(x, y))
qsort(nil) → nil
qsort(.(x, y)) → ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) → nil
lowers(x, .(y, z)) → if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) → nil
greaters(x, .(y, z)) → if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
LOWERS(x, .(y, z)) → LOWERS(x, z)
GREATERS(x, .(y, z)) → GREATERS(x, z)
QSORT(.(x, y)) → GREATERS(x, y)
QSORT(.(x, y)) → LOWERS(x, y)
QSORT(.(x, y)) → QSORT(greaters(x, y))
QSORT(.(x, y)) → QSORT(lowers(x, y))
qsort(nil) → nil
qsort(.(x, y)) → ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) → nil
lowers(x, .(y, z)) → if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) → nil
greaters(x, .(y, z)) → if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
GREATERS(x, .(y, z)) → GREATERS(x, z)
qsort(nil) → nil
qsort(.(x, y)) → ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) → nil
lowers(x, .(y, z)) → if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) → nil
greaters(x, .(y, z)) → if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GREATERS(x, .(y, z)) → GREATERS(x, z)
The value of delta used in the strict ordering is 8.
POL(GREATERS(x1, x2)) = (4)x_2
POL(.(x1, x2)) = 2 + (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
qsort(nil) → nil
qsort(.(x, y)) → ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) → nil
lowers(x, .(y, z)) → if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) → nil
greaters(x, .(y, z)) → if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
LOWERS(x, .(y, z)) → LOWERS(x, z)
qsort(nil) → nil
qsort(.(x, y)) → ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) → nil
lowers(x, .(y, z)) → if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) → nil
greaters(x, .(y, z)) → if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LOWERS(x, .(y, z)) → LOWERS(x, z)
The value of delta used in the strict ordering is 1.
POL(.(x1, x2)) = 1/4 + (4)x_2
POL(LOWERS(x1, x2)) = (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
qsort(nil) → nil
qsort(.(x, y)) → ++(qsort(lowers(x, y)), .(x, qsort(greaters(x, y))))
lowers(x, nil) → nil
lowers(x, .(y, z)) → if(<=(y, x), .(y, lowers(x, z)), lowers(x, z))
greaters(x, nil) → nil
greaters(x, .(y, z)) → if(<=(y, x), greaters(x, z), .(y, greaters(x, z)))